The present disclosure relates to model checking in general, and to reductions utilized prior to performing model checking in particular.
Computerized devices are an important part of the modern life. They control almost every aspect of our life—from writing documents to controlling traffic lights. However, computerized devices are bug-prone, and thus require a verification phase during which bugs should be discovered. The verification phase is considered one of the most difficult tasks in developing a computerized device. Many developers of computerized devices invest a significant portion, such as 70%, of the development cycle to discover erroneous behaviors of the computerized device, also referred to as a target computerized system. The target computerized system may comprise hardware, software, firmware, a combination thereof and the like.
During the verification phase, model checking techniques may be utilized to verify that a property is held by the target computerized system. The target computerized system is represented using a model. The model comprises a formal definition of state variables representing a state of the model. Each state variable is associated with a domain, such as for example a Boolean domain. The number of the variables and the size of their respective domains determine a number of possible states of the model, also referred to as a size of a model. The bigger the number of state, the less likely model checking may be completed before suffering from the “space-state explosion problem”.
In order to reduce a size of a model, reductions may be performed prior to performing model checking. Reductions may remove design redundancies from the model without substantially changing the model. A design redundancy may enlarge a size of a model without adding “interesting” states, such as reachable states which are substantially different from other reachable states. For example, if the model comprises a reachable state that does not hold a property, a modified model, determined by a reduction, must also comprise a corresponding reachable state that does not hold the property. It will be noted that in some cases, reductions may be performed in respect to a predetermined property and may yield different results based on different properties.
An exemplary design redundancy may be a variable associated with a surplus domain, such as a domain that comprises a value that is never assigned to the variable. Another exemplary design redundancy may be a state variable whose value may be computed based on values of other variables, and therefore may be removed from the state and transformed to a non-state variable, also referred to as a combinatorial signal, representing a computation of a value based on the other variables. Yet another exemplary design redundancy may be an unobservable variable which has no affect on an output of the model. For example, a variable V may be unobservable in case in every cycle its value is used only with an OR operator with a 1 value.